#include "ksat.h"
#include <stdio.h>
#include <stdlib.h>

/* X <> Y, T = True ; X = Y, T = false */
void setup_turnover(int X, int Y, int T, struct ksat *ksat)
{
	int list[3];

	list[0] = -X; list[1] =  Y; list[2] =  T;
	add_clause (ksat, 3, list);

	list[0] =  X; list[1] = -Y; list[2] =  T;
	add_clause (ksat, 3, list);

	list[0] =  X; list[1] =  Y; list[2] = -T;
	add_clause (ksat, 3, list);

	list[0] = -X; list[1] = -Y; list[2] = -T;
	add_clause (ksat, 3, list);
}

/* C00 : C[m][n] ; C10 : C[m-1][n] ; C11 : C[m-1][n-1] ; T : T[m] */
/* C[m][n] = C[m-1][n]bar_T[m] + C[m-1][n-1]T[m] */
void step_formula0 (int C00, int C10, int C11, int T, struct ksat *ksat)
{
	int list[3];

	list[0] =  C00; list[1] = -C10; list[2] =  T;
	add_clause (ksat, 3, list);

	list[0] =  C00; list[1] = -C11; list[2] = -T;
	add_clause (ksat, 3, list);

	list[0] = -C00; list[1] =  C10; list[2] =  C11;
	add_clause (ksat, 3, list);

	list[0] = -C00; list[1] =  C10; list[2] =  T;
	add_clause (ksat, 3, list);

	list[0] = -C00; list[1] =  C11; list[2] = -T;
	add_clause (ksat, 3, list);
}

/* C0 : C[m][0] ; C1 : C[m-1][0] ; T : T[m] */
/* C[m][0] = C[m-1][0]bar_T[m] */
void step_formula1 (int C0, int C1, int T, struct ksat *ksat)
{
	int list[3];

	list[0] =  C0; list[1] = -C1; list[2] =  T;
	add_clause (ksat, 3, list);

	list[0] = -C0; list[1] =  C1;
	add_clause (ksat, 2, list);

	list[0] = -C0; list[1] = -T;
	add_clause (ksat, 2, list);
}

/* C0 : C[m][m] ; C1 : C[m-1][m-1] ; T : T[m] */
/* C[m][m] = C[m-1][m-1]T[m] */
void step_formula2 (int C0, int C1, int T, struct ksat *ksat)
{
	int list[3];

	list[0] =  C0; list[1] = -C1; list[2] = -T;
	add_clause (ksat, 3, list);

	list[0] = -C0; list[1] =  C1;
	add_clause (ksat, 2, list);

	list[0] = -C0; list[1] =  T;
	add_clause (ksat, 2, list);
}

/* requiring among T[L] only num variables are true */
/* C[i][j] is true: among T[0],...T[i-1] only j variables are true */
void counter_positive1 (int L, int T[L], int num, int num2, int C[L + 1][num2 + 1], struct ksat *ksat)
{
	int list[3];
	int i, j, m, n, base;

	if (num > L)
	{
		printf ("impossible\n");
		exit (-1);
	}

	base = ksat->num_variables;

	/* setup the no. of logical variable C */
	for (i = 0; i < L; i++)
	{
		for (j = 0; j < num + 1; j++)
		{
			C[i + 1][j] = base + i * (num + 1) + j;
		}
	}

	/* setup the initial value */
	if (num)
		C[1][1] = T[0];

	list[0] =  C[1][0]; list[1] =  T[0];
	add_clause (ksat, 2, list);

	list[0] = -C[1][0]; list[1] = -T[0];
	add_clause (ksat, 2, list);

	for (i = 2; i <= L - num; i++)
	{
		step_formula1 (C[i][0], C[i - 1][0], T[i - 1], ksat);
	}

	list[0] =  C[L][num];
	add_clause (ksat, 1, list);

	/* setup the step formula */
	for (i = 0; i < num; i++)
	{
		m = L - i;
		if (m < 2)
			break;
		for (j = 0; j <= i; j++)
		{
			n = num - j;
			if (n > 0)
			{
				if (m > n)
				{
					step_formula0 (C[m][n], C[m - 1][n], C[m - 1][n - 1], T[m - 1], ksat);
				}
				else if (m == n && m > 1)
				{
					step_formula2 (C[m][n], C[m - 1][n - 1], T[m - 1], ksat);
				}
			}
		}
	}

	for (i = L - num; i >= 2; i--)
	{
		m = i;
		for (j = 1; j <= num; j++)
		{
			n = j;
			if (m > n)
				step_formula0 (C[m][n], C[m - 1][n], C[m - 1][n - 1], T[m - 1], ksat);
			else if (m == n)
				step_formula2 (C[m][n], C[m - 1][n - 1], T[m - 1], ksat);
			else if (m < n)
				break;
		}
	}

	ksat->num_variables += L * (num + 1);
}

/* requiring among T[L] no more than num variables are true */
/* C[i][j] is true: among T[0],...T[i-1] only j variables are true */
void counter_positive2 (int L, int T[L], int num, int num2, int C[L + 1][num2 + 1], struct ksat *ksat)
{
	int list[num + 1];
	int i, j, m, n, base;

	if (num >= L)
		return;

	base = ksat->num_variables;

	/* setup the no. of logical variable C */
	for (i = 0; i < L; i++)
	{
		for (j = 0; j < num + 1; j++)
		{
			C[i + 1][j] = base + i * (num + 1) + j;
		}
	}

	/* setup the initial value */
	if (num)
		C[1][1] = T[0];

	list[0] =  C[1][0]; list[1] =  T[0];
	add_clause (ksat, 2, list);

	list[0] = -C[1][0]; list[1] = -T[0];
	add_clause (ksat, 2, list);

	for (i = 2; i <= L; i++)
	{
		step_formula1 (C[i][0], C[i - 1][0], T[i - 1], ksat);
	}

	for (i = 0; i <= num; i++)
		list[i] =  C[L][i];
	add_clause (ksat, num + 1, list);

	/* setup the step formula */
	for (i = L; i >= 2; i--)
	{
		m = i;
		for (j = 1; j <= num; j++)
		{
			n = j;
			if (m > n)
				step_formula0 (C[m][n], C[m - 1][n], C[m - 1][n - 1], T[m - 1], ksat);
			else if (m == n)
				step_formula2 (C[m][n], C[m - 1][n - 1], T[m - 1], ksat);
			else if (m < n)
				break;
		}
	}

	ksat->num_variables += L * (num + 1);
}

/* requiring that the appearance of 1 in X array is earlier than Y array */
void check_order1 (int N, int X[N], int Y[N], struct ksat *ksat)
{
	int i, F[N], base, list[3];

	base = ksat->num_variables;

	for (i = 0; i < N; i++)
	{
		F[i] = base + i;
	}
	
	/* setup the variable F[N - 1] */
	list[0] =  F[N - 1]; list[1] = -X[N - 1]; list[2] = Y[N - 1];
	add_clause (ksat, 3, list);

	list[0] = -F[N - 1]; list[1] =  X[N - 1];
	add_clause (ksat, 2, list);

	list[0] = -F[N - 1]; list[1] = -Y[N - 1];
	add_clause (ksat, 2, list);

	/* setup the variable F[i] */
	for (i = 0; i < N - 1; i++)
	{
		list[0] =  F[i]; list[1] = -X[i]; list[2] =  Y[i];
		add_clause (ksat, 3, list);

		list[0] =  F[i]; list[1] =  Y[i]; list[2] = -F[i + 1];
		add_clause (ksat, 3, list);

		list[0] = -F[i]; list[1] =  X[i]; list[2] =  F[i + 1];
		add_clause (ksat, 3, list);

		list[0] = -F[i]; list[1] = -Y[i];
		add_clause (ksat, 2, list);
	}

	/* require F[0] = 1 */
	list[0] =  F[0];
	add_clause (ksat, 1, list);

	ksat->num_variables += N;
}

/* requiring that the appearance of 1 in X array is not later than Y array */
void check_order2 (int N, int Y[N], int X[N], struct ksat *ksat)
{
	int i, F[N], base, list[3];

	base = ksat->num_variables;

	for (i = 0; i < N; i++)
	{
		F[i] = base + i;
	}
	
	/* setup the variable F[N - 1] */
	list[0] =  F[N - 1]; list[1] = -X[N - 1]; list[2] =  Y[N - 1];
	add_clause (ksat, 3, list);

	list[0] = -F[N - 1]; list[1] =  X[N - 1]; 
	add_clause (ksat, 2, list);

	list[0] = -F[N - 1]; list[1] = -Y[N - 1]; 
	add_clause (ksat, 2, list);

	/* setup the variable F[i] */
	for (i = 0; i < N - 1; i++)
	{
		list[0] =  F[i]; list[1] = -X[i]; list[2] = Y[i];
		add_clause (ksat, 3, list);

		list[0] =  F[i]; list[1] =  Y[i]; list[2] = -F[i + 1];
		add_clause (ksat, 3, list);

		list[0] = -F[i]; list[1] =  X[i]; list[2] =  F[i + 1];
		add_clause (ksat, 3, list);

		list[0] = -F[i]; list[1] = -Y[i];
		add_clause (ksat, 2, list);
	}

	/* require F[0] = 0 */
	list[0] = -F[0];
	add_clause (ksat, 1, list);

	ksat->num_variables += N;
}
